Nuprl Lemma : R-Dsys-Rall
0,22
postcript
pdf
L
:Top List,
R
:Top. [[
x
L
.
R
(
x
)]] ~ reduce(
x
,
y
. [[
R
(
x
)]]
y
;;
L
)
latex
Definitions
x
:
A
.
B
(
x
)
,
Top
,
[[
R
]]
,
reduce(
f
;
k
;
as
)
,
x
.
t
(
x
)
,
t
T
,
Y
,
x
(
s
)
Lemmas
Rall-nil
,
Rall-cons
,
top
wf
origin
L:Top List, R:Top. [[
x
L.R(x)]] ~ reduce(
x,y. [[R(x)]] y;;L) L:Top List, R:Top. [[xL.R(x)]] ~ reduce(x,y. [[R(x)]] y;;L) x:A. B(x)
x. t(x) T